∂30-DEC-74  1345		THE,AJT
 John: 
 	I've read  the proposal draft,  and it  looks quite good  to me. But  it
 doesn't say  anything about a domain of mathematical  reasoning that I have been
 working on, viz.   geometry. I have come to  the conclusion that thinking  about
 geometry is  a good doamin for  analysing mathematical reasoning for  2 reasons:
 the  first is that  geometry is  a well-inderstood domain,  with many well-known
 axiomatizations (none of which turn out to be directly useable in FOL because of
 various interesting  metamathematical restrictions which I'm  working on getting
 around); secondly,  it is  a domain  where a  common technique  is to  use  real
 Ecuclidean space as a model for various axiomatic systems, and show the validity
 of various  propositions by example. This second thing seems  to be a good place
 to use the technique of semantic simplification aggressively.  And of course, it
 is my firm belief that any robot which  is going to reason about actions, &c. in
 first-order logic is also going to need to use logic to analyse its perceptions;
 so, by working on projective geometry, I hope to be  killing both a mathematical
 bird and a perceptual bird with one giant boulder. 
 
 	Incidentally, I don't  know whether you have left  it out, for political
 reasons, but  the  reason semantic  simplification  got  going was  that  I  was
 interested in  using an "eye"  which is much  more powerful than  the chess-eye,
 viz. a  TV camera. I believe that  this will be a fruitful  way of exploring the
 interaction between reasoning and perception. FOL will, in the very near future,
 be able to use hand-eye programs for gaining information. 
 
 	The sequel is an  extract from some notes I have on  what I'm doing. You
 may find it useful... 
 
 	This will  be an attempt to explore, using FOL, the expression and proof
 of some interesting propositions and theorems in elementary projective geometry,
 i.e.  a  geometry in which incidence is  invariant under stretching, translation
 and rotation  of the  plane.  Clearly, projective  geometry  is central  to  the
 question of visual perception, but its exact importance has not been explored in
 some systematic way. 
 
 	The  approach   is  two-fold,  involving  both  synthetic  and  analytic
 reasoning.   The  synthetic  approach  starts  from the  axioms  for  an  affine
 projective plane, and  adding Desargues' Axiom, Fano's Axiom  and Pappus' Axiom,
 results  in the proof of  the Fundamental Thoerem  of Projective Geometry, which
 says that there  exists a unique  projectivity from a  line L into itself  which
 sends three given  points, A,B,C into three other given  points.  Along the way,
 the notions  of projectvity  and  prespectivity are  defined,  and then  we  can
 proceed to  explore projective  collineations.   The analytic approach  proceeds
 hand in  hand with the synthetic.  For example,  Desargues' Axiom takes the form
 of a  `theorem' which  can be  shown  to hold  by an  argument which  shows  its
 validity in  a model, the real  projective plane.(In fact of  course, as Hilbert
 showed,  Desargues' theorem is  central not  only to the  question of projective
 geometry, but also to the  generation of analytic geometry.) The  linkup between
 the  analytic and  synthetic is  acheived  by aggressive  use of  the  notion of
 semantic simplification.  Starting with an  algebaric object, such as a field  F
 or the real numbers, R.   We define P(F) as a triples of  elements of the field,
 with a certain  equivalence relation defined on them, and define lines as linear
 equations.  We can  then define automorphisms of  P(F), automorphisms of F,  and
 show  the  validity  of  a  theorem   which  states  that  these  two  kinds  of
 automorphisms  generate the entire group of automorphisms  of P(F).  We can then
 show that the synthetically defined projective plane is a form  of P(F) for some
 division F  just in case  Desargues' axiom holds.   Further, Fano's  and Pappus'
 axioms are equivalent to algebraic statements about F.